ds:(IdType), da:(IdKndType), A:Type, X:Interface(ds;da;A).
interface-inr(X)  Interface(ds;da;{x:Top + A| (isl(x))} ) 

latex

Definitions	Top, t  T, left + right, f(a), x:AB(x), Type, x:A  B(x), a:A fp B(a), Atom$n, Id, Knd, let x,y = A in B(x;y), False, P  Q, A, b, inr x , x:A. B(x), isl(x), {x:A| B(x)} , Void, inl x , x.A(x), f o g  , let i,k:LocKnd = ik in P(i;k), LocKnd, hasloc(k;i), x,y. t(x;y), (x  l), type List, x:A.B(x), x. t(x), g o f, interface-inr(X), Interface(ds;da;A)
Lemmas	fpf-compose wf, l member wf, LocKnd wf, locknd-spread wf2, hasloc wf, Knd wf, Id wf, p-compose wf, not wf, assert wf, isl wf, false wf, top wf